(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** Matrix Multiplication *)
Require Import List.
Require Import Matrix.Mat.Mat_def.
Require Import Matrix.Mat.list_function.
Require Import Matrix.Mat.Mat_IO.
Require Import Matrix.Mat.Mat_map.
Require Import Matrix.Mat.Mat_add.
Require Import Matrix.Mat.Mat_trans.
Require Import Matrix.Mat.Mat_mult.


Section Mul.
Variable A:Set.
Variable Zero:A.
Variable One:A.
Variable add:A->A->A.
Variable mul:A->A->A.


(** * The Properties of Matrix Multiplication *)

Section Mul_lemma.

(** ** Distribution Law of Matrix Multiplication :(A+B)C = AC+BC *)

(** *** product_distr_l *)
(** Left distributive law of product : 
    (a+b)*c = a*c + b*c. *)
Lemma product_distr_l : forall(f:A->A->A) n a b c , 
  length a = n -> length b = n -> length c = n -> 
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c , mul (f a b)c = f (mul a c) (mul b c))->
  product' A Zero add mul (list_each A f a b) c 
  = f (product' A Zero add mul a c) (product' A Zero add mul b c).
Proof.
  induction n.
  induction a.
  induction b.
  simpl. intros. rewrite H2. auto.
  induction c. simpl. intros. rewrite H2. auto. simpl. intros. inversion H0.
  simpl. intros. inversion H.
  induction a. simpl. intros. inversion H.
  induction b. simpl. intros. inversion H0.
  induction c. simpl. intros. rewrite H2. auto. intros. simpl. rewrite H3.
  f_equal. apply H4. apply IHn. inversion H. auto. inversion H0. auto. 
  inversion H1. auto. apply H2. apply H3. apply H4.
Qed.

(** *** l_mul_dl_distr*)
(** Left distributive law of l_mul_dl : 
    ( l1 + l2 ) * ma = l1 * ma + l2 * ma. *)
Lemma l_mul_dl_distr : forall (f:A->A->A)(n:nat) (a b:list A) (c:list(list A)) , 
  length a = n -> length b = n -> width c n -> 
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c , mul (f a b)c = f (mul a c) (mul b c))->
  l_mul_dl A Zero add mul (list_each A f a b) c 
  = list_each A f (l_mul_dl A Zero add mul a c) 
    (l_mul_dl A Zero add mul b c).
Proof.
  induction n.
  induction a.
  induction b.
  induction c.
  auto. intros.  simpl. f_equal. rewrite H2.
  auto. assert (nil = list_each A add nil nil). simpl. auto. rewrite H5.
  apply IHc;auto. inversion H1. apply H7. simpl. intros. inversion H0.
  simpl. intros. inversion H. induction a. simpl. intros. inversion H. 
  induction b. simpl. intros. inversion H0. induction c. simpl. intros. 
  auto. intros. induction a2. inversion H1. inversion H5. simpl. f_equal. 
  rewrite H3. f_equal. apply H4. apply product_distr_l with (n:= n). inversion H. 
  auto. inversion H0. auto. inversion H1. inversion H5. auto. apply H2. 
  auto. auto. apply IHc;auto. inversion H1. auto.
Qed.

(** *** dl_mul_dl_distr_l *)
(** Left distributive law of dl_mul_dl :
    ( ma + mb ) * mc = ma * mc + mb * mc. *)
Lemma dl_mul_dl_distr_l : forall(f:A->A->A) (m n p:nat) (a b c:list(list A)),
  height a = m -> height b = m -> height c = p -> 
  width a n -> width b n -> width c n ->  
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c , mul (f a b)c = f (mul a c) (mul b c))->
  dl_mul_dl A Zero add mul ( mat_each' A f a b) c 
  = mat_each' A f (dl_mul_dl A Zero add mul a c)
    (dl_mul_dl A Zero add mul b c).
Proof.
  induction m.
  induction n.
  induction p.
  induction a. auto.
  induction b. auto.
  induction c. intros. inversion H. intros. inversion H.
  induction a. auto.
  induction b. auto.
  induction c. intros. inversion H. intros. inversion H.
  induction p. induction a. auto. induction b. auto. induction c. 
  intros. inversion H. intros. inversion H. induction a. auto. 
  induction b. auto. induction c. intros. inversion H. intros. 
  inversion H. induction n. induction p. induction a. auto. induction b. 
  auto. induction c. simpl. intros. f_equal. apply IHm with (n:=0)(p:=0). 
  inversion H. auto. inversion H0. auto. auto. apply H2. apply H3. auto. 
  auto. auto. auto. simpl. intros. inversion H1. induction a. auto. 
  induction b. auto. induction c. simpl. intros. inversion H1. simpl. 
  intros. f_equal. f_equal. apply product_distr_l with (n:= 0). apply H2. 
  apply H3. apply H4. auto. auto. auto.  apply l_mul_dl_distr with (n:=0). 
  apply H2. apply H3. apply H4. auto. auto. auto. apply IHm with (n:=0)(p:=S p). 
  inversion H. auto. inversion H0. auto. apply H1. apply H2. apply H3. simpl. 
  apply H4. auto. auto. auto. induction p. induction a. auto. induction b. 
  auto. induction c. simpl. intros. f_equal. apply IHm with (n:= S n)(p:=0). 
  inversion H. auto. inversion H0. auto. auto. apply H2. apply H3. auto. auto. 
  auto. auto. simpl. intros. inversion H1. induction a. auto. induction b. 
  auto. induction c. intros. inversion H1. simpl. intros. f_equal. f_equal. 
  apply product_distr_l with (n:= S n). apply H2. apply H3. apply H4. auto. 
  auto. auto. apply l_mul_dl_distr with (n:=S n). apply H2. apply H3. apply H4. 
  auto. auto. auto. apply IHm with (n:= S n)(p:= S p). inversion H. auto. 
  inversion H0. auto. apply H1. apply H2. apply H3. apply H4. auto. auto. auto.
Qed.

(** ** matrix_mul_distr_l *)
(** Left distribution law of mat_mul_mat : 
    ( A + B ) * C = A * C + B * C. *)
Lemma matrix_mul_distr_l : forall{f:A->A->A}{m n p:nat} 
  (a b: @Mat A m n) (c:@Mat A n p), 
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c , mul (f a b)c = f (mul a c) (mul b c))->
  matrix_mul A Zero add mul( matrix_each A f a b) c ===
  matrix_each A f (matrix_mul A Zero add mul a c)
  (matrix_mul A Zero add mul b c).
Proof.
  intros.
  induction a.
  induction b.
  induction c.
  unfold M_eq. simpl. unfold matrix_each. 
  unfold mat_each. simpl. unfold mat_mul_mat. simpl. 
  apply dl_mul_dl_distr_l with (m:=m) (n:=n)(p:=p);auto. apply height_gettrans. 
  apply width_gettrans. auto.
Qed.


(** ** Distribution Law of Matrix Multiplication :A(B+C) = AB + AC **)

(** *** product_distr_r *)
(** Right distribution law of product' : 
    a*(b+c) = a*b + a*c. *)
Lemma product_distr_r : forall(f:A->A->A) n (a b c:list A) , 
  length a = n -> length b = n -> length c = n -> 
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c , mul a (f b c) = f (mul a b) (mul a c))->
  product' A Zero add mul a (list_each A f b c) 
  = f (product' A Zero add mul a b) (product' A Zero add mul a c).
Proof.
  induction n.
  induction a.
  induction b.
  simpl. intros. rewrite H2. auto.
  induction c. simpl. intros. rewrite H2. auto. simpl. intros. inversion H0.
  simpl. intros. inversion H.
  induction a. simpl. intros. inversion H.
  induction b. simpl. intros. inversion H0.
  induction c. simpl. intros. rewrite H2. auto. inversion H1. 
  intros. simpl. rewrite H3.
  f_equal. apply H4. apply IHn. inversion H. auto. inversion H0. auto. 
  inversion H1. auto. apply H2. apply H3. apply H4.
Qed.

(** *** l_mul_dl_distr_r *)
(** Right distribution law of l_mul_dl : 
   l1 * ( ma + mb ) = l1 * ma + l1 * mb **)
Lemma l_mul_dl_distr_r : forall(f:A->A->A) m n (a:list A) (b c:list(list A)) , 
  length a = n -> width b n -> width c n ->
  height b = m -> height c = m ->
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c , mul a (f b c) = f (mul a b) (mul a c))->
  l_mul_dl A Zero add mul a (mat_each' A f b c) 
  = list_each A f (l_mul_dl A Zero add mul a b) (l_mul_dl A Zero add mul a c).
Proof.
  induction m.
  - induction n.
    + induction a.
      * induction b. auto. induction c. auto. intros. inversion H2.
      * induction b. auto. induction c. auto. intros. inversion H2.
    + induction a.
      * induction b. auto. induction c. auto. intros. inversion H3.
      * induction b. auto. induction c. auto. intros. inversion H2.
  - induction n.
    + induction a.
      * induction b. auto. induction c. auto. intros. simpl. rewrite H4.
        f_equal. apply IHm with (n:=0). apply H. inversion H0. apply H8.
        inversion H1. apply H8. inversion H2. auto. inversion H3. auto.
        apply H4. apply H5. apply H6.
      * induction b. auto. induction c. auto. intros. inversion H.
    + induction a.
      * intros. inversion H.
      * induction b. intros. inversion H2. induction c. intros.
        inversion H3. induction a1. intros. inversion H0. inversion H7.
        induction a2. intros. inversion H1. inversion H7.
        intros. simpl. rewrite H5. rewrite H6. f_equal. f_equal. 
        rewrite product_distr_r with (n:= n). f_equal.
        inversion H. auto. inversion H0. inversion H7. auto.
        inversion H1. inversion H7. auto. apply H4. apply H5.
        apply H6. apply IHm with(n:=S n). apply H. inversion H0. apply H8. 
        inversion H1. apply H8. inversion H2. auto. inversion H3. auto.
        apply H4. apply H5. apply H6.
Qed.


(** *** dl_mul_dl_distr_r *)

Lemma dl_mul_dl_distr_r : forall(f:A->A->A) m n (a b c:list(list A)),
  width a n -> width b n -> width c n ->
  height b = m -> height c = m ->
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c , mul a (f b c) = f (mul a b) (mul a c))->
  dl_mul_dl A Zero add mul a ( mat_each' A f b c) 
  = mat_each' A f (dl_mul_dl A Zero add mul a b)(dl_mul_dl A Zero add mul a c).
Proof.
  induction n.
  - induction a. intros. auto. induction a. simpl. intros. 
      rewrite l_mul_dl_distr_r with(m:= m)(n:=0).
      f_equal. apply IHa. apply H. apply H0. apply H1. apply H2. apply H3.
      apply H4. apply H5. apply H6. auto. apply H0. apply H1. apply H2.
      apply H3. apply H4. apply H5. apply H6. intros. inversion H. inversion H7.
  - induction a. simpl. auto. induction a. intros. inversion H. inversion H7.
    intros. simpl. rewrite l_mul_dl_distr_r with(m:=m) (n:=S n).
    f_equal. apply IHa. inversion H. apply H8. apply H0. apply H1.
    apply H2. apply H3. apply H4. apply H5. apply H6. inversion H.
    apply H7. apply H0. apply H1. apply H2. apply H3. apply H4. apply H5.
    apply H6.
Qed. 

(** ** matrix_mul_distr_l *)
(** Right distribution law of mat_mul_mat : 
    A * ( B + C )  = A * B + A * C. *)
Lemma matrix_mul_distr_r : forall{f:A->A->A}{m n p:nat} (a: @Mat A m n) (b c:@Mat A n p),
  (forall a , f a Zero = a) ->
  (forall a b c d , f (add a b) (add c d) = add (f a c) (f b d))-> 
  (forall a b c , mul a (f b c) = f (mul a b) (mul a c))->
  matrix_mul A Zero add mul a ( matrix_each A f b c) ===
  matrix_each A f (matrix_mul A Zero add mul a b) 
  (matrix_mul A Zero add mul a c).
Proof.
  induction a.
  induction b.
  induction c.
  unfold M_eq. simpl. unfold matrix_each. 
  unfold mat_each. simpl. unfold mat_mul_mat. simpl. intros. 
  rewrite gettrans_mat_each' with(m:=n). 
  apply dl_mul_dl_distr_r with (m:=p) (n:=n);auto. apply width_gettrans.
  apply mat_height0. apply width_gettrans. apply mat_height1.
  apply height_gettrans. apply height_gettrans. apply mat_height0.
  apply mat_height1. apply mat_width0. apply mat_width1.
  apply H.
Qed.

Lemma product'_zero_l: forall m a,  
  length a = m ->
  (forall a,mul Zero a = Zero) ->
  (forall a,add Zero a = a) ->
  product' A Zero add mul (list_o A Zero m)
  a = Zero.
Proof.
  induction m. simpl. auto.
  induction a. intros. inversion H. intros.
  simpl. rewrite H0. rewrite H1. apply IHm. inversion H. auto. auto.
  auto.
Qed.

Lemma list_mul_zero_l: forall m n ma,
  length ma = m -> width ma n ->
   (forall a,mul Zero a = Zero) ->
  (forall a,add Zero a = a) ->
  l_mul_dl A Zero add mul (list_o A Zero n) ma =
  list_o A Zero m.
Proof.
  induction m. induction ma. intros. simpl. auto.
  intros. inversion H. induction ma. intros. inversion H.
  intros. simpl. f_equal. apply product'_zero_l.
  apply H0. auto. auto. apply IHm. inversion H. 
  auto. apply H0. auto. auto.
Qed.

Lemma dlist_mul_zero_l:forall m n p (ma:list(list A)),
  height ma = p -> width ma n->
  (forall a,mul Zero a = Zero) ->
  (forall a,add Zero a = a) ->
  dl_mul_dl A Zero add mul (dlist_o A Zero m n) ma 
  = (dlist_o A Zero m p).
Proof.
  induction m. simpl. auto.
  induction p. 
  - induction ma. intros. rewrite dl_mul_dl_nil with(m:=S m).
    rewrite dlist_o_m_0. auto. apply dlist_o_height.
    intros. inversion H.
  - induction ma. intros. inversion H.
    intros. simpl. f_equal. f_equal. apply product'_zero_l.
    apply H0. auto. auto. apply list_mul_zero_l.
    inversion H. auto. apply H0. auto. auto. apply IHm.
    auto. apply H0. auto. auto.
Qed.

Lemma matrix_mul_zero_l: forall m n p (ma:Mat A n p),
  (forall a,mul Zero a = Zero) ->
  (forall a,add Zero a = a) ->
  matrix_mul A Zero add mul (MO A Zero m n) ma === MO A Zero m p.
Proof.
  unfold matrix_mul,mat_mul_mat,MO,M_eq. simpl. 
  intros. apply dlist_mul_zero_l.
  apply height_gettrans. apply width_gettrans.
  apply (mat_height A n p ma).
  auto. auto.
Qed.

Lemma head_list_o: forall m,
  @hd A Zero (list_o A Zero m) = Zero.
Proof.
  induction m. simpl. auto.
  simpl. auto.
Qed.

Lemma headcolumn_dlist_o: forall m n,
  headcolumn A Zero (dlist_o A Zero m n) = list_o A Zero m.
Proof.
  induction m. simpl. auto.
  simpl. intros. f_equal. apply head_list_o.
  apply IHm. 
Qed.

Lemma tailcolumn_dlist_o: forall m n,
  tailcolumn A (dlist_o A Zero m (S n)) = dlist_o A Zero m n.
Proof.
  induction m. simpl. auto.
  intros. simpl. f_equal. apply IHm.
Qed.

Lemma product'_zero_r: forall m a,  
  length a = m ->
  (forall a,mul a Zero = Zero) ->
  (forall a,add Zero a = a) ->
  product' A Zero add mul a (list_o A Zero m) = Zero.
Proof.
  induction m.
  induction a. intros. simpl. auto. intros. inversion H. 
  induction a. intros. inversion H. intros.
  simpl. rewrite H0. rewrite H1. apply IHm. inversion H. auto. auto.
  auto.
Qed.

Lemma list_mul_zero_r: forall n p a,
  length a = n ->
  (forall a,mul a Zero = Zero) ->
  (forall a,add Zero a = a) ->
  l_mul_dl A Zero add mul a (dlist_o A Zero p n) 
  = list_o A Zero p.
Proof.
  induction p. intros. simpl. auto.
  - induction n. induction a. intros. simpl. f_equal.
    rewrite dlist_o_m_0. rewrite l_mul_dl_nil_list.
    auto. intros. inversion H. induction a.
    intros. inversion H. intros. simpl.
    f_equal. rewrite H0,H1. apply product'_zero_r.
    inversion H. auto. auto. auto. apply IHp.
    auto. auto. auto.
Qed.


Lemma dlist_mul_zero_r:forall p m n (ma:list(list A)),
  height ma = m -> width ma n->
  (forall a b : A, mul a b = mul b a)->
  (forall a0 : A, mul a0 Zero = Zero)->
  (forall a0 : A, add Zero a0 = a0 ) ->
  dl_mul_dl A Zero add mul ma 
  (dlist_o A Zero p n) = (dlist_o A Zero m p).
Proof.
  induction p. simpl. intros. rewrite dl_mul_dl_nil with(m:=m).
  rewrite dlist_o_m_0. auto. auto.
  induction m. - induction ma. intros. simpl. auto.
  intros. inversion H. - induction ma. intros. inversion H.
  intros. simpl. f_equal. f_equal. apply product'_zero_r.
  apply H0. auto. auto. apply list_mul_zero_r. apply H0.
  auto. auto. assert(list_o A Zero n :: dlist_o A Zero p n=
  dlist_o A Zero (S p) n). { auto. }
  rewrite H4. rewrite IHm. auto. auto. apply H0.
  auto. auto. auto.
Qed.

Lemma matrix_mul_zero_r: forall m n p (ma:Mat A m n),
  (forall a b : A, mul a b = mul b a)->
  (forall a0 : A, mul a0 Zero = Zero)->
  (forall a0 : A, add Zero a0 = a0 ) ->
  matrix_mul A Zero add mul ma (MO A Zero n p) === MO A Zero m p.
Proof.
  unfold matrix_mul,mat_mul_mat,MO,M_eq. simpl. 
  intros. rewrite gettrans_dlist_o. apply dlist_mul_zero_r.
  apply (mat_height A m n ma).
  apply (mat_width A m n ma). auto. auto. auto.
Qed.

Lemma product'_nil: forall a,
  product' A Zero add mul a nil= Zero.
Proof.
  induction a. simpl. auto.
  simpl. auto.
Qed.

Lemma gettrans_nil_list: forall m n,
  gettrans A Zero (nil_list A m) n = 
  dlist_o A Zero n m.
Proof.
  induction m. simpl. intros. rewrite gettrans_nil.
  rewrite dlist_o_m_0. auto.
  induction n. simpl. auto.
  simpl. f_equal. rewrite headcolumn_nil_list. auto.
  rewrite <- IHn. f_equal. simpl. rewrite tailcolumn_nil_list.
  auto.
Qed. 


Lemma mul_product'_l:forall h a d e,
  length d = h -> length e = h ->
   (forall a, mul a Zero = Zero) ->
  (forall a b c, mul a(add b c) =add (mul a b) (mul a c))-> 
  (forall a b c,mul a (mul b c) = mul b (mul a c)) ->
  mul a (product' A Zero add mul d e) =
  product' A Zero add mul d (c_mul_l A mul a e).
Proof.
  induction h.
  induction d. intros. simpl. auto.
  induction e. intros. simpl. auto.
  intros. inversion H.
  induction d. intros. inversion H.
  induction e. intros. inversion H0.
  intros. simpl. rewrite <-IHh. rewrite H3.
  rewrite <-H2. auto. inversion H. auto. inversion H0.
  auto. auto. auto. auto.
Qed.

Lemma mul_product'_r:forall h a d e,
  length d = h -> length e = h ->
   (forall a, mul Zero a = Zero) ->
  (forall a b c, mul (add b c) a =add (mul b a) (mul c a))-> 
  (forall a b c,mul a (mul b c) = mul (mul a c) b) ->
  mul (product' A Zero add mul d e) a =
  product' A Zero add mul d (c_mul_l A mul a e).
Proof.
  induction h.
  induction d. intros. simpl. auto.
  induction e. intros. simpl. auto.
  intros. inversion H.
  induction d. intros. inversion H.
  induction e. intros. inversion H0.
  intros. simpl. rewrite <-IHh. rewrite H2.
  rewrite <-H3. auto. inversion H. auto. inversion H0.
  auto. auto. auto. auto.
Qed.

Lemma list_each_nil: forall l1,
  list_each A add l1 nil = nil.
Proof.
  induction l1. simpl. auto.
  simpl. auto.
Qed.

Lemma l_mul_dl_gettrans_cons: forall h w a b c mb,
  height mb = h -> length b = h ->
  length c = w -> width mb w -> 
  l_mul_dl A Zero add mul (a :: b) 
  (gettrans A Zero (c :: mb) w) =
  list_each A add (c_mul_l A mul a c)
  (l_mul_dl A Zero add mul b (gettrans A Zero mb w)).
Proof.
  induction h. induction w. intros. simpl. rewrite list_each_nil.
  auto.
  induction b,mb. induction c. intros. inversion H1.
   rewrite gettrans_nil.
  rewrite l_mul_dl_nil_list. intros. simpl. f_equal. rewrite IHw.
  f_equal. rewrite gettrans_nil. rewrite l_mul_dl_nil_list.
  auto. auto. auto. inversion H1. auto. auto. intros. inversion H.
  intros. inversion H0. intros. inversion H.
  induction w. simpl. intros. rewrite list_each_nil. auto.
  induction c. intros. inversion H1. induction mb.
  intros. inversion H. induction b. intros. inversion H0.
  intros. simpl. f_equal. rewrite IHw. auto. simpl.
  f_equal. apply height_tailcolumn. inversion H. auto.
  auto. inversion H1. auto. simpl. split.
  apply length_tl. apply H2. apply width_tailcolumn.
  apply H2.
Qed.

Lemma c_mul_l_headcolumn: forall c mb,
  (forall a, mul a Zero = Zero) ->
  (forall a, add a Zero = a) ->
  c_mul_l A mul c (headcolumn A Zero mb) =
  l_mul_dl A Zero add mul (c :: nil) mb.
Proof.
  induction mb. simpl. auto.
  induction a. simpl. intros. rewrite H. f_equal.
  apply IHmb. auto. auto. intros. simpl.
  f_equal. rewrite H0. auto. apply IHmb. auto. auto.
Qed.
  
Lemma add_product': forall h a b c,
  length a = h -> length b = h -> length c = h -> 
   (forall a, add Zero a = a) ->
  (forall a b c d, add (add a b) (add c d) 
    = add (add a c) (add b d)) ->
  (forall a b c ,add (mul a b) (mul a c) =mul a ( add b c))->
  add(product' A Zero add mul a b)(product' A Zero add mul a c)= 
  product' A Zero add mul a (list_each A add b c).
Proof.
  induction h.
  induction a. simpl. intros. rewrite H2. auto.
  intros. inversion H.
  induction a. intros. inversion H. induction b.
  intros. inversion H0. induction c. intros.
  inversion H1. intros.
  simpl. rewrite H3. rewrite H4. f_equal.
  apply IHh. inversion H. auto. inversion H0. auto.
  inversion H1. auto. auto. auto. auto.
Qed.

Lemma list_each_c_mul_l:forall mb a b, 
  (forall a, mul a Zero = Zero) -> 
  (forall a, add a Zero = a) ->
  list_each A add (c_mul_l A mul a (headcolumn A Zero mb))
  (l_mul_dl A Zero add mul b (tailcolumn A mb)) =
  l_mul_dl A Zero add mul (a::b) mb.
Proof.
  induction mb. simpl. auto.
  induction a. simpl. intros. f_equal.
  rewrite product'_nil. rewrite H. apply H0.
  apply IHmb. auto. auto. intros. simpl.
  f_equal. rewrite IHmb. auto. auto. auto.
Qed. 

Lemma tm1: forall h w a b c d e mb,
  length a = S h -> height mb = h ->
  length d = w -> length e = w -> width mb (S w) -> 
  (forall a, add a Zero = a) ->
  (forall a, mul a Zero = Zero) ->
  (forall a, mul Zero a = Zero) ->
  (forall a, add Zero a = a) ->
  (forall a b c, mul (mul a b) c = mul a (mul b c)) ->
  (forall a b c, mul a(add b c) =add (mul a b) (mul a c))-> 
  (forall a b : A, mul a b = mul b a)->
  (forall a b c : A,
    mul (add b c) a = add (mul b a) (mul c a)) ->
  (forall a b c d : A,
  add (add a b) (add c d) = add (add a c) (add b d)) ->
  add (mul (product' A Zero add mul a (b :: headcolumn A Zero mb)) c)
  (product' A Zero add mul (l_mul_dl A Zero add mul a
        (gettrans A Zero (e :: tailcolumn A mb) w)) d) =
    product' A Zero add mul a
    (add (mul c b)(product' A Zero add mul d e) 
      :: l_mul_dl A Zero add mul (c :: d) mb).
Proof.
  induction h.
  - induction a. intros. inversion H. induction mb.
    intros. simpl. rewrite product'_nil. rewrite ?H4.
  induction w. induction d,e. simpl.
    rewrite ?H4. rewrite H8. rewrite H10 with(a:=c). auto.
    inversion H2. inversion H1. inversion H1.
    induction d,e. inversion H1. inversion H1. inversion H2.
    simpl. rewrite product'_nil. rewrite H4. 
    rewrite H9. rewrite H10 with(a:=c). rewrite H8. f_equal. 
    rewrite H9. f_equal. rewrite H8. rewrite H10 with (a:=a1).
    auto. rewrite product'_comm .
    rewrite mul_product'_l with(h:=w). f_equal.
    rewrite l_mul_dl_gettrans_cons with(h:=0).
    rewrite gettrans_nil. rewrite l_mul_dl_nil_list.
    rewrite list_add_zero_r. auto. auto. rewrite length_c_mul_l.
    inversion H2. auto. auto. inversion H. auto. inversion H2.
    auto. auto. inversion H1. auto. auto. auto. auto.
    intros. rewrite <- H8. rewrite H10 with(a:=a3). auto. auto.
    intros. inversion H0.
  - induction w. induction d,e. intros. simpl. 
    rewrite ?H4. rewrite mul_product'_r with(h:=S(S h)).
    f_equal. simpl. f_equal. apply c_mul_l_headcolumn.
    auto. auto. auto. simpl. f_equal. apply length_headcolumn.
    auto. auto. auto. intros. rewrite H10 with(a:= b0).
    rewrite H8. auto. intros. inversion H2.
    intros. inversion H1. intros. inversion H1.
    induction d,e. intros. inversion H1. intros. inversion H1.
    intros. inversion H2. intros. simpl. rewrite IHw.
    rewrite mul_product'_r with(h:= S(S h)).
    rewrite add_product' with(h:=S(S h)).
    f_equal. simpl. f_equal. apply list_each_c_mul_l.
    auto. auto. auto. rewrite length_c_mul_l. simpl.
    f_equal. apply length_headcolumn. auto.
    simpl. f_equal. rewrite length_l_mul_dl.
    apply height_tailcolumn. auto. auto.
    auto. auto. auto. simpl. f_equal. apply length_headcolumn.
    auto. auto. auto. intros. rewrite H10 with(a:=b0).
    rewrite H8. auto. auto. apply height_tailcolumn.
    auto. inversion H1. auto. inversion H2. auto.
    apply width_tailcolumn. auto. auto. auto. auto.
    auto. auto. auto. auto. auto. auto. 
Qed.
   

Lemma l_mul_dl_cons: forall h w a b mb,
  length a = w -> length b = w ->
  height mb = h ->
  l_mul_dl A Zero add mul a (b::mb) = 
  (product' A Zero add mul a b)
  ::l_mul_dl A Zero add mul a mb.
Proof.
  induction w. induction a. induction b.
  intros. simpl. auto.
  intros. inversion H0. intros. inversion H.
  induction h. induction mb. simpl. auto.
  intros. inversion H1. induction a. intros.
  inversion H. induction b. intros. inversion H0.
  induction mb. intros. inversion H1.
  intros. simpl. f_equal.
Qed.
  

Lemma l_mul_dl_assoc: forall n p k a mb mc,
  length a = n -> height mb =n ->
  width mb p ->  height mc = k -> width mc p ->
  (forall a, add a Zero = a) ->
  (forall a b c,mul (mul a b) c = mul a (mul b c))->
  (forall a, mul a Zero = Zero) ->
  (forall a, mul Zero a = Zero) ->
  (forall a, add Zero a = a) ->
  (forall a b c, mul a(add b c) =add (mul a b) (mul a c))-> 
  (forall a b, mul a b = mul b a)->
  (forall a b c, mul (add a b) c = add (mul a c) (mul b c)) ->
  (forall a b c d,
  add (add a b) (add c d) = add (add a c) (add b d)) ->
  l_mul_dl A Zero add mul
  (l_mul_dl A Zero add mul a (gettrans A Zero mb p)) mc =
  l_mul_dl A Zero add mul a (dl_mul_dl A Zero add mul mc mb).
Proof.
  induction n.
  - induction mb. intros. simpl. rewrite ?gettrans_nil.
    rewrite dl_mul_dl_nil with(m:= k). rewrite ?l_mul_dl_nil_list.
    rewrite list_mul_zero_l with(m:= k). auto.
    auto. auto. auto. auto. auto. intros. inversion H0.  
  - induction p.
    intros. simpl. apply width_dlist_0 with(m:=S n) in H1.
    rewrite H1. rewrite dl_mul_dl_nil_list_r with(m:= k).
    rewrite l_mul_dl_nil with(m:= k). rewrite list_mul_zero_r.  
    auto. auto. auto. auto. auto. auto. auto. auto.
    induction k. induction mc. simpl. auto.
    intros.  inversion H2. 
    induction mb. intros. inversion H0.
    induction mc. intros. inversion H2.
    intros. induction a1. inversion H3. inversion H13.
    induction a0. inversion H1. inversion H13.
    simpl. f_equal. apply tm1 with(h:= n). auto. 
    inversion H0. auto. inversion H3. inversion H13.
    auto. inversion H1. inversion H13. auto. apply H1. auto.
    auto. auto. auto. auto. auto. auto. auto. auto.
    rewrite  <-IHk. f_equal. auto. auto. auto.
    inversion H2. auto. apply H3. auto. auto.
    auto. auto. auto. auto. auto. auto. auto.
Qed.

Lemma dl_mul_dl_assoc: forall m n p k ma mb mc,
  height ma = m -> width ma n ->
  height mb = n -> width mb p ->
  height mc = k -> width mc p ->
  (forall a, add a Zero = a) ->
  (forall a b c,mul (mul a b) c = mul a (mul b c))->
  (forall a, mul a Zero = Zero) ->
  (forall a, mul Zero a = Zero) ->
  (forall a, add Zero a = a) ->
  (forall a b c, mul a(add b c) =add (mul a b) (mul a c))-> 
  (forall a b : A, mul a b = mul b a)->
  (forall a b c : A,
    mul (add a b) c = add (mul a c) (mul b c)) ->
  (forall a b c d : A,
  add (add a b) (add c d) = add (add a c) (add b d)) ->
  dl_mul_dl A Zero add mul
  (dl_mul_dl A Zero add mul ma
  (gettrans A Zero mb p))
  mc  =
  dl_mul_dl A Zero add mul ma
  (dl_mul_dl A Zero add mul mc mb).
Proof.
  induction m.
  - induction ma. auto. intros. inversion H.
  - induction ma. intros. inversion H.
    intros. simpl. f_equal. apply l_mul_dl_assoc with(n:=n)(k:=k) .
    apply H0. auto. auto. auto. auto. auto. auto. auto. auto.
    auto. auto. auto. auto. auto. auto. 
    apply IHm with(n:= n)(k:=k). inversion H. auto. apply H0.
    auto. auto. auto. auto. auto. auto. auto. auto. auto.
    auto. auto. auto. auto. 
Qed.
  



(** ** matrix_mul_distr_l *)
(** Associative law of matrix_mul : 
    A * ( B * C )  = A * ( B * C ). *)
Lemma matrix_mul_assoc : forall{m n p k:nat} (a: @Mat A m n) (b:@Mat A n p)
  (c:@Mat A p k ),
   (forall a, add a Zero = a) ->
  (forall a b c,mul (mul a b) c = mul a (mul b c))->
  (forall a, mul a Zero = Zero) ->
  (forall a, mul Zero a = Zero) ->
  (forall a, add Zero a = a) ->
  (forall a b c, mul a(add b c) =add (mul a b) (mul a c))-> 
  (forall a b, mul a b = mul b a)->
  (forall a b c,mul (add a b) c = add (mul a c) (mul b c)) ->
  (forall a b c d ,
  add (add a b) (add c d) = add (add a c) (add b d)) ->
  matrix_mul A Zero add mul ( matrix_mul A Zero add mul a b) c ===
  matrix_mul A Zero add mul a (matrix_mul A Zero add mul b c) .
Proof.
  intros. unfold M_eq,matrix_mul,mat_mul_mat. simpl.
  rewrite dl_mul_dl_gettrans_r with(m:=n) (n:=p)(ma:=mat A n p b).
  rewrite trans_same. 
  rewrite dl_mul_dl_gettrans_r with(m:=m)(n:=n)(ma:=mat A m n a).
  rewrite dl_mul_dl_gettrans_l with(n:=m)(p:=n)(mb:=mat A m n a).
  rewrite trans_same.
  rewrite <- dl_mul_dl_assoc with(m:= m)(n:=n)(p:=p)(k:=k).
  auto. apply (mat_height A m n a).
  apply (mat_width A m n a). apply (mat_height A n p b).
  apply (mat_width A n p b). apply height_gettrans.
  apply width_gettrans. apply (mat_height A p k c).
  auto. intros. rewrite H0. auto. auto. auto. auto.
  auto. auto. auto. auto.
  rewrite height_dl_mul_dl. apply (mat_height A m n a).
  apply width_dl_mul_dl. apply height_gettrans.
  auto. apply (mat_height A n p b). apply (mat_width A n p b).
  apply (mat_height A m n a). apply (mat_width A m n a).
  auto. apply (mat_height A m n a). apply (mat_width A m n a). 
  apply (mat_height A n p b). apply (mat_width A n p b).
  rewrite height_dl_mul_dl. apply height_gettrans. 
  apply width_dl_mul_dl. apply (mat_height A n p b).
  auto. apply (mat_height A n p b). apply (mat_width A n p b). 
  apply (mat_height A p k c). apply (mat_width A p k c).
Qed.
  
  
   
  

(** * The Properties of Multiplying Constant and Matrix *)

(** ** Matrix number multiplication communication law: cA = Ac *)

(** *** c_mul_l_comm *)
(** Communicative law of c_mul_l and l_mul_c : c * l = l * c. *)
Lemma c_mul_l_comm : forall c (l:list A),
  (forall a b , mul a b = mul b a) ->
  c_mul_l A mul c l = l_mul_c A mul c l.
Proof.
  induction l.
  - intros. simpl. reflexivity.
  - intros. simpl. rewrite H. f_equal. apply IHl. apply H.
Qed.

(** *** c_mul_dl_comm *)
(** Communicative law of c_mul_dl and dl_mul_c: c * m = m * c. **)
Lemma c_mul_dl_comm : forall c (m:list (list A)),
  (forall a b , mul a b = mul b a) ->
  c_mul_dl A mul c m = dl_mul_c A mul c m.
Proof.
  induction m.
  - intros. simpl. reflexivity.
  - intros. simpl. f_equal. rewrite c_mul_l_comm with (c:=c) (l:=a).
    f_equal. apply H. apply IHm.
    apply H. 
Qed.

(** *** c_mul_mat_comm *)
(** Communicative law of c_mul_mat and mat_mul_c: c * M = M * c. *)
Lemma c_mul_mat_comm : forall c (m n:nat) (ma:@Mat A m n),
  (forall a b , mul a b = mul b a) ->
  c_mul_mat A mul c ma = mat_mul_c A mul c ma.
Proof.
  unfold c_mul_mat,mat_mul_c. intros.
  apply c_mul_dl_comm. apply H.
Qed.

(** ** const_mul_comm *)
(** Communicative law of const_mul_l and const_mul_r: c * M = M * c. *)
Lemma const_mul_comm : forall {m n:nat} c (ma:@Mat A m n),
  (forall a b , mul a b = mul b a) ->
  const_mul_l A mul c ma === const_mul_r A mul c ma.
Proof.
  unfold M_eq. simpl. intros. apply c_mul_mat_comm. apply H.
Qed.

(** ** Right Distribution Law of Matrix Multiplication: 
       c(A+B) = cA + cB *)

(** *** c_mul_l_distr_r *)
(** Right distribution law of c_mul_l : c * ( l1 + l2 ) = cl1 + cl2. *)
Lemma c_mul_l_distr_r : forall c (l1 l2: list A),
  (forall a b c, mul a (add b c) = add (mul a b) (mul a c))->
  c_mul_l A mul c (list_each A add l1 l2) 
  = list_each A add (c_mul_l A mul c l1)(c_mul_l A mul c l2).
Proof.
  induction l1.
  - induction l2.
    + intros. simpl. auto.
    + intros. simpl. auto.
  - induction l2.
    + intros. simpl. auto.
    + intros. simpl. rewrite H. f_equal. apply IHl1.
      apply H.
Qed.

(** *** c_mul_dl_distr_r *)
(** Right distribution law of c_mul_dl : 
    c * ( dl1 + dl2 ) = c * dl1 + c * dl2.**)
Lemma c_mul_dl_distr_r : forall c (ma1 ma2:list(list A)) ,
  (forall a b c, mul a (add b c) = add (mul a b) (mul a c))->
  c_mul_dl A mul c (mat_each' A add ma1 ma2) 
  = mat_each' A add (c_mul_dl A mul c ma1) (c_mul_dl A mul c ma2).
Proof.
  induction ma1.
  - induction ma2.
    + intros. simpl. reflexivity.
    + intros. simpl. reflexivity.
  - induction ma2.
    + intros. simpl. reflexivity.
    + intros. simpl. rewrite c_mul_l_distr_r. f_equal.
      apply IHma1. apply H. apply H.
Qed.

(** *** c_mul_mat_distr_r *)
(** Right distribution law of c_mul_mat : 
    c * ( M1 + M2 ) = c * M1 + c * M2. *)
Lemma c_mul_mat_distr_r : forall c m n (ma1 ma2:@Mat A m n) ,
  (forall a b c, mul a (add b c) = add (mul a b) (mul a c))->
  c_mul_mat A mul c (matrix_each A add ma1 ma2) 
  = mat_each' A add (c_mul_mat A mul c ma1) (c_mul_mat A mul c ma2).
Proof.
  intros.
  unfold c_mul_mat. simpl.
  unfold mat_each. apply c_mul_dl_distr_r.
  apply H.
Qed.

(** ** const_mul_l_distr_r *)
(** Right distribution law of const_mul_l : c(A+B) = c*A+c*B **)
Lemma const_mul_l_distr_r : forall {m n:nat} c (ma1 ma2:@Mat A m n),
  (forall a b c, mul a (add b c) = add (mul a b) (mul a c))->
  const_mul_l A mul c (matrix_each A add ma1 ma2) ===
  matrix_each A add (const_mul_l A mul c ma1) (const_mul_l A mul c ma2).
Proof.
  unfold M_eq. simpl.
  unfold c_mul_mat. simpl.
  unfold mat_each. simpl. intros. apply c_mul_mat_distr_r. apply H.
Qed.

(** ** Left Distribution Law of Matrix Multiplication : 
       ( c1 + c2 ) * A = c1 * A + c2 * A *)

(** *** c_mul_l_distr_l *)
(** Left distribution law of c_mul_l : 
    ( c1 + c2 ) * l = c1 * l + c2 * l. *)
Lemma c_mul_l_distr_l : forall (c1 c2:A) (l1:list A) ,
  (forall a b c, mul (add a b) c = add (mul a c) (mul b c))->
  c_mul_l A mul (add c1 c2 ) l1
  = list_each A add (c_mul_l A mul c1 l1) (c_mul_l A mul c2 l1).
Proof.
  induction l1.
  - intros. simpl. auto.
  - intros. simpl. auto. rewrite H. f_equal.
     apply IHl1. apply H.
Qed.

(** *** c_mul_dl_distr_l *)
(**  Left distribution law of c_mul_dl : 
    ( c1 + c2 ) m = c1 * m + c2 * m. *)
Lemma c_mul_dl_distr_l : forall(c1 c2:A) (ma:list(list A)) ,
  (forall a b c, mul (add a b) c = add (mul a c) (mul b c))->
  c_mul_dl A mul (add c1 c2) ma
  = mat_each' A add (c_mul_dl A mul c1 ma) (c_mul_dl A mul c2 ma).
Proof.
  induction ma.
  - intros. simpl. reflexivity.
  - intros. simpl. rewrite c_mul_l_distr_l. f_equal. apply IHma.
    apply H. apply H.
Qed.

(** *** c_mul_mat_distr_l *)
(** Left distribution law of c_mul_mat : 
    ( c1 + c2 ) * m = c1 * m + c2 * m. *)
Lemma c_mul_mat_distr_l : forall c1 c2 m n (ma:@Mat A m n) ,
  (forall a b c, mul (add a b) c = add (mul a c) (mul b c))->
  c_mul_mat A mul (add c1 c2) ma
  = mat_each' A add (c_mul_mat A mul c1 ma) (c_mul_mat A mul c2 ma).
Proof.
  unfold c_mul_mat. 
  intros. simpl. apply c_mul_dl_distr_l. apply H. 
Qed.

(** *** const_mul_l_distr_l *)
(** Left distribution law of const_mul_l : 
    ( c1 + c2 ) * M = c1 * M + c2 * M. *)
Lemma const_mul_l_distr_l : forall {m n:nat} c1 c2  (ma:@Mat A m n),
  (forall a b c, mul (add a b) c = add (mul a c) (mul b c))->
  const_mul_l A mul (add c1 c2) ma === 
  matrix_each A add (const_mul_l A mul c1 ma)(const_mul_l A mul c2 ma).
Proof.
  unfold M_eq. simpl. unfold mat_each. simpl. 
  intros. apply c_mul_mat_distr_l. apply H.
Qed.

(** ** Left Associative Law of Matrix Multiplication : 
       ( c1 * c2) A = c1 * ( c2 * A ). **)

(** *** c_mul_l_comb *)
(** The left associative law of c_mul_l : 
    ( c1 * c2) * l = c1 * ( c2 * l ). *)
Lemma c_mul_l_comb : forall c1 c2 (l:list A),
  (forall a b c ,mul (mul a  b) c = mul a (mul b c))->
  c_mul_l A mul (mul c1 c2) l = c_mul_l A mul c1 (c_mul_l A mul c2 l).
Proof.
  induction l.
  - intros. simpl. reflexivity.
  - intros. simpl. rewrite H. f_equal. apply IHl.  apply H.
Qed.

(** *** c_mul_dl_comb *)
(** The left associative law of c_mul_dl : 
    ( c1 * c2) * dl = c1 * ( c2 * dl ). *)
Lemma c_mul_dl_comb : forall c1 c2 (dl:list(list A)),
  (forall a b c ,mul (mul a  b) c = mul a (mul b c))->
  c_mul_dl A mul (mul c1 c2) dl = c_mul_dl A mul c1 (c_mul_dl A mul c2 dl).
Proof.
  induction dl.
  - intros. simpl. reflexivity.
  - intros. simpl. rewrite c_mul_l_comb. f_equal.
    apply IHdl. apply H. apply H.
Qed.

(** *** c_mul_mat_comb *)
(** The left associative law of c_mul_dl : 
    ( c1 * c2) * M = c1 * ( c2 * M ). *)
Lemma c_mul_mat_comb: forall c1 c2 m n (ma:@Mat A m n),
  (forall a b c, mul( mul a b) c = mul a (mul b c))->
  c_mul_mat A mul (mul c1 c2) ma 
  = c_mul_dl A mul c1 (c_mul_mat A mul c2 ma).
Proof.
  intros. unfold c_mul_mat. apply c_mul_dl_comb. apply H.
Qed.

(** ** const_mul_l_assoc_l *)
(** Left associative law of const_mul_l : 
    ( c1 * c2 ) * A = c1 * ( c2 * A ). *)
Lemma const_mul_l_assoc_l : forall {m n :nat} c1 c2 (ma:@Mat A m n),
  (forall a b c, mul( mul a b) c = mul a (mul b c))->
  (const_mul_l A mul (mul c1 c2)  ma) ===
  (const_mul_l A mul c1 (const_mul_l A mul c2 ma)).
Proof.
  unfold M_eq,const_mul_l. simpl. unfold c_mul_mat. simpl.
  intros. apply c_mul_mat_comb. apply H.
Qed.

(** ** Matrix Number Multiplication Law: 0*A = O **)

(** *** c_mul_l_0_l *)
(** 0 * l = lzero. *)
Lemma c_mul_l_0_l : forall m (l:list A),
  (forall a, mul Zero a = Zero)->
  (length l = m)->
  c_mul_l A mul Zero l = list_o A Zero m.
Proof.
  induction m.
  - induction l.
    + intros. simpl. reflexivity.
    + intros. simpl in H0. discriminate H0.
  - induction l.
    + intros. simpl in H0. discriminate H0.
    + intros. simpl. rewrite H. f_equal. apply IHm.
      apply H. inversion H0. reflexivity.
Qed.

(** *** c_mul_dl_0_l *)
(** 0 * dl = dlzero. *)
Lemma c_mul_dl_0_l : forall m n (ma:list(list A)) ,
  (height ma = m) ->
  (width ma n)->
  (forall a, mul Zero a = Zero)->
  c_mul_dl A mul Zero ma = dlist_o A Zero m n.
Proof.
  induction m.
  - induction n.
    + induction ma.
      * intros. simpl. reflexivity.
      * intros. inversion H.
    + induction ma.
      * intros. simpl. reflexivity.
      * intros. inversion H.
  - induction n.
    + induction ma.
      * intros. inversion H.
      * intros. apply width_dlist_0 with (m:=S m) in H0.
        rewrite H0. simpl. f_equal. apply IHm. rewrite height_nil_list. reflexivity.
        apply width_nil_list. apply H1. apply H.
    + induction ma.
      * intros. inversion H.
      * intros. simpl. rewrite c_mul_l_0_l with(m:=S n).
        simpl. f_equal. apply IHm. inversion H. reflexivity.
        inversion H0. apply H3. apply H1. apply H1. inversion H. 
        inversion H0. apply H2.
Qed.

(** *** c_mul_mat_0_l *)
(** 0 * M = dlzero. *)
Lemma c_mul_mat_0_l: forall m n (ma:@Mat A m n),
  (forall a, mul Zero a = Zero)->
  c_mul_mat A mul Zero ma = dlist_o A Zero m n.
Proof.
  unfold c_mul_mat. intros. apply c_mul_dl_0_l.
  apply (mat_height A m n ma). apply (mat_width A m n ma).
  apply H.
Qed.

(** ** const_mul_l_0 *)
(** 0 * M = Mzero. *)
Lemma const_mul_l_0: forall {m n:nat} (ma:@Mat A m n),
   (forall a, mul Zero a = Zero)->
  const_mul_l A mul Zero ma  === MO A Zero m n .
Proof.
  unfold M_eq,const_mul_l,MO.
  simpl. intros. apply c_mul_mat_0_l.
  apply H.
Qed.

Lemma const_mul_r_0: forall {m n:nat} (ma:@Mat A m n),
   (forall a, mul Zero a = Zero)->
  (forall a b : A, mul a b = mul b a)->
  const_mul_r A mul Zero ma  === MO A Zero m n .
Proof.
  intros. rewrite <- const_mul_comm.
  rewrite const_mul_l_0. unfold M_eq. auto.
  auto. auto.
Qed.
  
(*
Lemma dl_mul_dl_rev_l:forall ma mb,
  dl_mul_dl A Zero add mul (rev ma) mb 
  = rev (dl_mul_dl A Zero add mul ma mb).
Proof.
  induction ma. intros. simpl. auto. induction mb.
  rewrite dl_mul_dl_nil with(m:= S(length ma)).
  rewrite dl_mul_dl_nil with(m:= S(length ma)).
  rewrite rev_nil_list. f_equal. simpl. auto.
  apply length_rev. simpl. auto. simpl.
  rewrite dl_mul_dl_app_l with(h1:= length ma)(h2:=1).
  f_equal. apply IHma. unfold height. rewrite length_rev with(m:=length ma).
  auto. auto. simpl. auto.
Qed.

Lemma l_mul_dl_One_nil: forall ma,
    (forall a, mul One a = a) ->
  (forall a, add a Zero = a) ->
  l_mul_dl A Zero add mul (One :: nil) ma = headcolumn A Zero ma.
Proof.
  induction ma. simpl. auto. intros.
  simpl. induction a. simpl. f_equal. auto.
  simpl. intros. rewrite H,H0. f_equal.
  auto. 
Qed.
*)

Lemma product'_unit_l:forall n i a,
  length a = n ->
  (forall a, mul Zero a = Zero)->
  (forall a, mul One a = a) ->
  (forall a, add a Zero = a) ->
  (forall a, add Zero a = a) ->
  product' A Zero add mul (list_i A Zero One n i) a =
  get_nth A Zero a i.
Proof.
  induction n,a. simpl. rewrite get_nth_nil. auto.
  intros. inversion H. intros. inversion H.
  intros. induction i. simpl. rewrite H0,H3. 
  rewrite list_i_n_0. rewrite product'_zero_l.
  auto. inversion H. auto. auto. auto.
  simpl. induction i. simpl. rewrite H1.
  rewrite list_i_n_0. rewrite product'_zero_l. auto.
  inversion H. auto. auto. auto. simpl.
  rewrite H0,H3. rewrite IHn. simpl. auto. inversion H.
  auto. auto. auto. auto. auto.
Qed.
(*
Lemma list_mul_unit_l: forall n (ma:list(list A)),
  width ma n ->
  (forall a, mul Zero a = Zero)->
  (forall a, mul One a = a) ->
  (forall a, add a Zero = a) ->
  (forall a, add Zero a = a) ->
  l_mul_dl A Zero add mul (list_i A Zero One n n) ma =
  column_nth A Zero ma n.
Proof.
  induction n. intros.
  apply width_dlist_0 with(m:=(length ma))in H.
  rewrite H. rewrite column_nth_nil_list. 
  rewrite l_mul_dl_nil_list. auto. auto.
  induction ma. simpl. auto.
  intros. assert(l_mul_dl A Zero add mul 
  (list_i A Zero One (S n) (S n)) (a :: ma) = 
  product' A Zero add mul (list_i A Zero One (S n) (S n))a::
  l_mul_dl A Zero add mul (list_i A Zero One (S n) (S n)) ma).
  { auto. } rewrite H4.
  assert(column_nth A Zero (a :: ma) (S n) = 
  get_nth A Zero a (S n) :: column_nth A Zero ma (S n)).
  { auto. } rewrite H5. f_equal.
  apply product'_unit_l. apply H. auto. auto. auto. auto.
  apply IHma. apply H. auto. auto. auto. auto.
Qed.*)
(*
Lemma rev_dlist_o: forall m n,
  rev(dlist_o A Zero m n) = dlist_o A Zero m n.
Proof.
  induction m. simpl. auto.
  induction n. simpl. rewrite IHm. rewrite dlist_o_m_0.
  assert(nil::nil= nil_list A 1). auto. rewrite H.
  rewrite <-nil_list_app. rewrite S_plus_1. auto.
  simpl. rewrite IHm. assert((Zero :: list_o A Zero n)::nil 
  = dlist_o A Zero 1 (S n)). auto. rewrite H.
  rewrite <-dlist_o_app. rewrite S_plus_1. auto.
Qed.*)
(*
Lemma dlist_mul_unit_l':forall n i (ma:list(list A)),
   width ma n ->
  (forall a, mul One a = a) ->
  (forall a, add a Zero = a) ->
  dl_mul_dl A Zero add mul (dlist_i' A Zero One n i) ma =
  rev( gettrans A Zero (tailcolumn_n A ma i) i).
Proof.
  induction n. intros. apply width_dlist_0 with(m:= length ma) in H.
  rewrite H. rewrite dlist_i'_0_i. rewrite dl_mul_dl_nil_list_l with(n := length ma).
  rewrite tailcolumn_n_nil_list. rewrite gettrans_nil_list. auto.
  rewrite rev_dlist_o. auto. apply height_nil_list. auto.
  induction i. simpl. auto.
  intros. assert(dlist_i' A Zero One (S n) (S i) = 
  list_i A Zero One (S n) (S i) :: dlist_i' A Zero One (S n) i).
  simpl. auto. rewrite H2.
  assert(dl_mul_dl A Zero add mul
  (list_i A Zero One (S n) (S i) :: dlist_i' A Zero One (S n) i) ma
  = l_mul_dl A Zero add mul (list_i A Zero One (S n) (S i)) ma::
    dl_mul_dl A Zero add mul (dlist_i' A Zero One (S n) i) ma).
  { auto. } rewrite H3. 
Admitted.

Lemma dlist_mul_unit_l'':forall m n (ma:list(list A)),
  height ma = m -> width ma n ->
  (forall a, mul One a = a) ->
  (forall a, add a Zero = a) ->
  dl_mul_dl A Zero add mul (dlist_i' A Zero One n n) ma =
  rev( gettrans A Zero ma n).
Proof.
  induction n.
  simpl. auto. 
  intros. assert(dlist_i' A Zero One (S n) (S n) =
  list_i A Zero One (S n) (S n) :: dlist_i' A Zero One (S n) n).
  { simpl. auto. } rewrite H3.
  assert(dl_mul_dl A Zero add mul
  (list_i A Zero One (S n) (S n) :: dlist_i' A Zero One (S n) n) ma
  = l_mul_dl A Zero add mul (list_i A Zero One (S n) (S n)) ma::
    dl_mul_dl A Zero add mul (dlist_i' A Zero One (S n) n) ma).
  { auto. } rewrite H4. rewrite list_mul_unit_l.
  
  
  Admitted.

Lemma dlist_mul_unit_l: forall m n (ma:list(list A)),
  height ma = m -> width ma n ->
  dl_mul_dl A Zero add mul (rev (dlist_i' A Zero One n n))
  ma = gettrans A Zero ma n.
Proof.
  intros. rewrite dl_mul_dl_rev_l.
  Admitted.
*)

Lemma product'_unit_l':forall n a,
  length a = S n->
  (forall a,mul One a = a) ->
  (forall a,add a Zero = a) ->
  (forall a,mul Zero a = Zero)->
  (forall a,add Zero a = a) ->
  product' A Zero add mul (One :: list_i A Zero One n 0) a = hd Zero a.
Proof.
  induction n,a. intros. inversion H. intros. simpl.
  rewrite H0,H1. auto. intros. inversion H.
  intros. induction a0. simpl. rewrite H0,H1. auto.
  simpl. rewrite H0. rewrite H2,H3. rewrite list_i_n_0.
  rewrite product'_zero_l. auto. inversion H. auto. auto.
  auto.
Qed.

Lemma list_mul_unit_l': forall n ma,
  width ma (S n) ->
  (forall a,mul One a = a) ->
  (forall a,add a Zero = a) ->
  (forall a,mul Zero a = Zero)->
  (forall a,add Zero a = a) ->
  l_mul_dl A Zero add mul (One :: list_i A Zero One n 0) ma 
  = headcolumn A Zero ma.
Proof.
  induction ma. simpl. auto.
  intros. assert (l_mul_dl A Zero add mul 
  (One :: list_i A Zero One n 0) (a :: ma) = 
  product' A Zero add mul (One :: list_i A Zero One n 0) a::
  l_mul_dl A Zero add mul (One :: list_i A Zero One n 0) ma).
  { auto. } rewrite H4. 
  assert(headcolumn A Zero (a :: ma) = @hd A Zero a::
  headcolumn A Zero ma). { auto. } rewrite H5.
  f_equal. apply product'_unit_l'. apply H. auto.
  auto. auto. auto. apply IHma. apply H. auto. auto.
  auto. auto.
Qed.

Fixpoint link1 l (ma:list (list A)):=
  match l with
  |nil => ma
  |a::a' => match ma with
            |nil =>nil
            | x::x' => (a::x):: link1 a' x'
            end 
  end.
  

Lemma link1_nil_r: forall l,
  link1 l nil = nil.
Proof.
  induction l. simpl. auto. simpl. auto.
Qed.

Lemma height_link1:forall m l ma,
  height ma = m -> length l = m ->
  height (link1 l ma) = m.
Proof.
  induction m. induction l. induction ma. auto.
  intros. inversion H. intros. inversion H0.
  induction l. intros. inversion H0. induction ma.
  intros. inversion H. intros. simpl. f_equal.
  rewrite IHm. auto. inversion H. auto. inversion H0.
  auto.
Qed.

Lemma width_link1: forall m n l ma,
  height ma = m -> length l = m ->
  width ma n->
  width (link1 l ma) (S n).
Proof.
  induction m. induction l. induction ma. auto.
  intros. inversion H. intros. inversion H0.
  induction n. intros. apply width_dlist_0 with(m:=S m) in H1.
  rewrite H1. simpl.
  induction l. intros. inversion H0. induction ma.
  inversion H. simpl. split. auto. apply IHm. 
  apply height_nil_list. inversion H0. auto. apply width_nil_list.
  auto.
  induction l. intros. inversion H0. induction ma. intros.
  inversion H. intros. simpl. split. f_equal. apply H1.
  apply IHm. inversion H. auto. inversion H0. auto.
  apply H1.
Qed.
  

Lemma l_mul_dl_list_i:forall n ma,
  width ma (S(S n)) ->
   (forall a, mul Zero a = Zero) ->
  (forall a, add Zero a = a) ->
  (forall a, mul One a = a) ->
  (forall a, add a Zero = a) ->
  l_mul_dl A Zero add mul
  (Zero :: One :: list_i A Zero One n 0) ma =
  l_mul_dl A Zero add mul (One :: list_i A Zero One n 0)
  (tailcolumn A ma).
Proof.
  induction ma. simpl. auto.
  intros. induction a. inversion H. inversion H4.
  induction a0. simpl. f_equal. rewrite H0,H1. auto.
  rewrite IHma. auto. apply H. auto. auto. auto. auto.
  simpl. f_equal. rewrite H0,H2. rewrite H1. auto.
  rewrite IHma. auto. apply H. auto. auto. auto.
  auto.
Qed.

Lemma l_mul_dl_list_i':forall n i ma, 
  width ma (S(S n)) ->
  (forall a, mul Zero a = Zero) ->
  (forall a, add a Zero = a) ->
  (forall a, add Zero a = a) ->
  l_mul_dl A Zero add mul
  (Zero :: Zero :: list_i A Zero One n (S i)) ma =
l_mul_dl A Zero add mul
  (Zero :: list_i A Zero One n (S i))
  (tailcolumn A ma).
Proof.
  induction ma. simpl. auto.
  intros. induction a. inversion H. inversion H3. 
  induction a0. inversion H.
  inversion H3. simpl. f_equal. rewrite ?H0. rewrite ?H2.
  auto. apply IHma. apply H. auto. auto. auto.
Qed.

Lemma dlist_i'_link1: forall m n i,
  dlist_i' A Zero One m (S n) (S i) 
  = link1 (list_o A Zero m) ( dlist_i' A Zero One m n i).
Proof.
  induction m. simpl. auto.
  induction n. simpl. intros. f_equal. rewrite IHm. auto.
  induction i. simpl. f_equal. rewrite IHm. auto.
  simpl. f_equal. apply IHm.
Qed.

Lemma dlist_i'_m_0: forall m i,
  dlist_i' A Zero One m 0 i = nil_list A m.
Proof.
  induction m. simpl. auto.
  simpl. intros. f_equal. apply IHm.
Qed.
Lemma l_mul_dl_Zero_nil: forall ma,
  (forall a,mul Zero a = Zero) ->
  (forall a,add a Zero = a)->
  l_mul_dl A Zero add mul (Zero :: nil) ma =
  l_mul_dl A Zero add mul nil (tailcolumn A ma).
Proof.
  induction ma. simpl. auto. induction a. intros. simpl. f_equal.
  auto. intros. simpl. f_equal. rewrite H,H0. auto.
  apply IHma. auto. auto.
Qed.

Lemma link1_list_o_nil_list:forall m,
  link1 (list_o A Zero m) (nil_list A m) = dlist_o A Zero m 1.
Proof.
  induction m. simpl. auto.
  simpl. f_equal. apply IHm.
Qed.

Lemma dlist_mul_unit_l: forall m n i ma,
  width ma (S n) ->
  (forall a, mul Zero a = Zero) ->
  (forall a, add Zero a = a) ->
  (forall a, mul One a = a) ->
  (forall a, add a Zero = a) ->
  dl_mul_dl A Zero add mul (link1 (list_o A Zero m) (dlist_i' A Zero One m n i))
  ma = dl_mul_dl A Zero add mul (dlist_i' A Zero One m n i) (tailcolumn A ma).
Proof.
  induction m. simpl. intros. auto.
  induction n. simpl. intros. rewrite dlist_i'_m_0. 
  rewrite ?dl_mul_dl_nil_list_l with(n:=length ma). f_equal. 
  apply l_mul_dl_Zero_nil. auto. auto. 
  rewrite link1_list_o_nil_list. rewrite dlist_mul_zero_l with(p:=length ma).
  auto. auto. auto. auto. auto. apply height_tailcolumn. auto.
  induction i. simpl. intros. f_equal. apply l_mul_dl_list_i. auto.
  auto. auto. auto. auto. apply IHm. auto. auto. auto. auto. auto.
  simpl. intros. f_equal. apply l_mul_dl_list_i'. auto. auto.
  auto. auto. auto.
Qed.
  


  

Lemma dlist_mul_unit_l': forall m n (ma:list(list A)),
  height ma = m -> width ma n ->
  (forall a,mul One a = a) ->
  (forall a,add a Zero = a) ->
  (forall a,mul Zero a = Zero)->
  (forall a,add Zero a = a) ->
  dl_mul_dl A Zero add mul (dlist_i' A Zero One n n 0)
  ma = gettrans A Zero ma n.
Proof.
  induction n. simpl. auto.
  simpl. intros. f_equal.
  apply list_mul_unit_l'. auto. auto. auto. auto. auto.
  rewrite <-IHn. rewrite dlist_i'_link1. apply dlist_mul_unit_l.
  auto. auto. auto. auto. auto. apply height_tailcolumn. auto.
  apply width_tailcolumn. auto. auto. auto. auto. auto.
Qed.
   

(** ** matrix_mul_unit_l **)
(** The multplication of a matrix and a unit matrix equals to the matrix
    itself : ma * I = ma. *)
Lemma matrix_mul_unit_l : forall  {m n:nat} (ma:@Mat A m n),
  (forall a,mul One a = a) ->
  (forall a,add a Zero = a) ->
  (forall a,mul Zero a = Zero)->
  (forall a,add Zero a = a) ->
  matrix_mul A Zero add mul (MI A Zero One m) ma === ma.
Proof.
  intros.
  unfold matrix_mul,mat_mul_mat,MI,M_eq. simpl.
  rewrite dlist_mul_unit_l' with(m:= n).
  rewrite trans_same. auto. apply(mat_height A m n ma).
  apply (mat_width A m n ma). apply height_gettrans.
  apply width_gettrans. apply (mat_height A m n ma).
  auto. auto. auto. auto.
Qed.

Lemma headcolumn_dlist_i': forall n m i,
  headcolumn A Zero (dlist_i' A Zero One n m (S i))
  = list_i A Zero One n 0.
Proof.
  induction n. simpl. auto.
  induction m. simpl. intros. f_equal. apply IHn.
  induction i. simpl. f_equal. apply IHn.
  simpl. f_equal. apply IHn.
Qed.

Lemma tailcolumn_dlist_i': forall m n i,
  tailcolumn A (dlist_i' A Zero One m (S n) (S i)) =
  dlist_i' A Zero One m n i.
Proof.
  induction m. simpl. auto.
  induction n. simpl. intros. f_equal. apply IHm.
  induction i. simpl. f_equal. apply IHm.
  simpl. f_equal. apply IHm.
Qed. 

Lemma gettrans_link1: forall n a ma,
  length a = n -> width ma n ->
  gettrans A Zero (a::ma) n =link1 a (gettrans A Zero ma n).
Proof.
  induction n. induction a. simpl. auto.
  intros. inversion H. induction a. intros. inversion H.
  induction ma. intros. simpl. f_equal. apply IHn.
  inversion H. auto. auto.
  intros. simpl. f_equal.
  apply IHn. inversion H. auto. simpl.
  split. apply length_tl. apply H0. apply width_tailcolumn.
  apply H0.
Qed.
  
Lemma tailcolumn_link1:forall m a ma,
  length a = m -> height ma = m->
  tailcolumn A(link1 a ma) = ma.
Proof.
  induction m. induction a. induction ma. 
  simpl. auto. intros. inversion H0.
  intros. inversion H. 
  induction a. intros. inversion H.
  induction ma. intros. inversion H0.
  intros. simpl. f_equal. apply IHm.
  inversion H. auto. inversion H0. auto.
Qed.


Lemma gettrans_dlist_i' : forall n ,
  gettrans A Zero (dlist_i' A Zero One n n 0 )n 
  = dlist_i' A Zero One n n 0.
Proof.
  induction n. simpl. auto.
  simpl. f_equal. f_equal. apply headcolumn_dlist_i'.
  rewrite dlist_i'_link1. rewrite gettrans_link1.
  f_equal. apply list_i_n_0. rewrite tailcolumn_link1 with(m:=n).
  apply IHn. apply list_o_length. apply height_dlist_i'.
  apply length_list_i. apply width_tailcolumn. 
  apply width_link1 with(m:= n). apply height_dlist_i'.
  apply list_o_length. apply width_dlist_i'.
Qed.


Lemma trans_MI: forall n, trans A Zero ( MI A Zero One n) 
  === ( MI A Zero One n).
Proof.
  unfold trans,MI,M_eq. simpl. apply gettrans_dlist_i'.
Qed.
  

End Mul_lemma.
End Mul.